\documentclass{llncs}

\usepackage[utf8]{inputenc}
\usepackage{amssymb}
\usepackage{amsmath}
\usepackage{stmaryrd}
\usepackage{xcolor}
\usepackage{proof}
\usepackage{comment}
\usepackage{xspace}

\newcommand\red[1]{{\color{blue} #1}}
\newcommand\Sscr{\ensuremath{\mathcal{S}}}
\newcommand\ie{\emph{i.e.}\xspace}
\newcommand\eg{\emph{e.g.}\xspace}

% Tentative titles
% Automated Generation of Complete Focused Proof Systems
\title{Automated Generation of Focused Proof Systems}
\author{Vivek Nigam\inst{1} \and Giselle Reis\inst{2}}

\institute{Federal University of Para\'{i}ba, Brazil
\and Inria Saclay, France
}

%% Page limit: 15

\begin{document}
\maketitle

\begin{abstract}
This paper tackles the problem of formulating and proving the completeness of
focused-like proof systems in an automated fashion. Focusing is a discipline on
proofs where proofs are structured into phases in order to reduce proof search
non-determinism. This paper demonstrates that it is possible to construct a
complete focused proof system from a given un-focused proof system if it
satisfies some conditions. Our key idea is to generalize the completeness proof
based on permutation lemmas given by Miller and Saurin for the focused linear
logic proof system. We build a graph from the rule permutation relation of a
proof system, called Permutation Graph. We then show that from the permutation
graph of a given proof system, it is possible to construct a complete focused
proof system of it. We additionally show how to infer from the permutation graph
for which formulas contraction is admissible. We apply our technique to generate
the focused proof systems LLF, LJF and LKF for linear, intuitionistic and
classical logics, respectively.
\end{abstract}

\section{Introduction}

% TODO: fix references.
Focused proof systems were originally proposed by Andreoli~\cite{andreoli92jlc}
for linear logic~\cite{girard87tcs} and today there are also focused proof
systems for many other logics, \eg, classical, intuitionistic logics~\cite{liang07csl} and logics with
fixed points~\cite{baelde08phd}. Although initially introduced in order to
reduce the search space for proof search, focused proof systems have been
successfully used as logical frameworks for specifying deductive systems, such
as, the operational semantics of programming
languages~\cite{nigam09ppdp,pfenning09lics,nigam13concur,pfenning99cade} and proof systems~\cite{nigam10jar,miller13tcs,nigam14jlc}. Focusing is also in the
core of foundational proof certificates \cite{miller11cpp,miller07csla,chihani13cade}, making it possible
for certificates to inform only the necessary information for a proof checker
(the selection points, for example) and leave less relevant computation to be
done automatically by the checker itself.

In spite of its widespread use, the propositions and completeness
proofs of focused proof systems are still an \emph{ad-hoc} and hard task, done
for each individual system separately. For example, the original completeness
proof for the focused linear logic proof system (LLF)~\cite{andreoli92jlc} is
very specific to linear logic. The completeness proof for many focused proof
systems for intuitionistic logic, such as LJF~\cite{liang07csl}, LKQ and
LKT~\cite{danos93wll}, are obtained by using non-trivial encodings of
intuitionistic logic in linear logic.

One exception, however, is the work of Miller and Saurin~\cite{miller07cslb},
where they propose a modular way to prove the completeness of focused proof
systems based on permutation lemmas and proof transformations. One shows that a
given focused proof system is complete with respect to its unfocused version by
demonstrating that one can transform any proof in the unfocused system into a
proof in the focused system. Their proof technique has been successfully adapted
to prove the completeness of a number of focused proof systems based on
linear logic, such as ELL~\cite{danos03ic}, $\mu$MALL~\cite{baelde08phd} and
SELLF~\cite{nigam09phd}.

This paper investigates the automated generation of a sound and complete focused
proof system from a given unfocused sequent calculus proof system. Our approach
uses as theoretical foundations the modular proof given by Miller and
Saurin~\cite{miller07cslb}. There are, however, a number of challenges in
automating such a proof for any given unfocused proof system.

\begin{enumerate}
  \item Not all proof systems seem to admit a focused version\footnote{At
  least the existing methods for proving their completeness are not general
  enough.}. We propose sufficient conditions, which can be checked in an
  automated fashion, for a given proof  system to admit a focused one;

  \item Given a proof system that satisfies these conditions, one needs to
  formulate its focused version;

  \item Finally, Miller and Saurin's proof cannot be directly applied to proof
  systems that have contraction and weakening rules, such as
  LJ.\footnote{Miller and Saurin do handle full classical linear logic, but as
  exponentials, which allow contraction and weakening, are known to cause complications because of their
  dual polarity behavior, the solution proposed by Miller and Saurin is
  specific to linear logic.} Focused proof systems, such as LJF and LKF, allow
  only the contraction of some formulas.
  The admissibility of contraction on negative formulas is, for example, one of
  the features of LJF as it reduces considerably search space. This result was
  obtained by non-trivial encodings in linear logic mentioned
  above~\cite{liang09tcs}. Here, we demonstrate that this can be obtained in the
  system itself, \ie, without a detour through linear logic.
\end{enumerate}

In order to overcome these challenges, we introduce the notion of Permutation Graphs. 
A permutation graph of a proof system is a directed graph whose nodes are
inference rules and an edge from $r_1$ to $r_2$ denotes that $r_1$ permutes up
$r_2$. Our previous work~\cite{nigam13iclp,nigam14ijcar} showed how to check
whether a rule permutes over another in an automated fashion. We use these
results to construct the permutation graph of a proof system. This paper then
shows that by analysing the permutation graph of an unfocused proof system, we
can construct a focused version of it that is sound and complete. We also
demonstrate how to check the admissibility of contraction rules.
 
Finally, we should mention the technique proposed by Simmons~\cite{simmons.unp}
for proving the completeness of a focused proof system. His proof relies on
proving properties of the focused calculus, such as cut-elimination and
identity expansion, instead of analysing the permutation of inference rules. In this paper, we adopt the methodology introduced by Miller and Saurin based on permutation lemmas as these can easily be proved in an automated
fashion~\cite{nigam13iclp,nigam14ebl}, whereas it is not yet clear whether the properties used in Simmons proof can be inferred in \emph{an automated fashion}.
We leave as future work the investigation of inferring Simmons's proof in an automated fashion, possibly
relying on the techniques introduced in our previous work~\cite{nigam14jlc}.

We start in Section~\ref{sec:perm_graphs} by introducing Permutation Graphs and
explain in Section~\ref{sec:focusing} sufficient conditions for when a complete focused system can be
generated. 
Section~\ref{sec:contraction} describes how to infer when contraction is
admissible in a class of formulas. In Section~\ref{sec:cases}, we apply our
techniques to three systems: MALL, LJ and LK, obtaining the systems MALLF, LJF and
LKF in an automated fashion. We then finish in Section~\ref{sec:conc} by
pointing out future work.
 

\section{Permutation Graphs}
\label{sec:perm_graphs}

Our definition of focused proof systems tries to be general enough so that the
concept can be applied to a wide range of logics. We will prove the conditions
that a sequent calculus system must meet to have a focused version that is, sound and complete. In order to do that, we will rely on a structure
called \emph{permutation graph}. This graph can be used to obtain the rules for
each phase of focusing (Section \ref{sec:focusing}) and also to reason about the
admissibility of contraction (Section \ref{sec:contraction}).

In the following we assume that we are given a sequent calculus proof system
$\mathbb{S}$ which is is commutative, that is, sequents are formed by mutisets
of formulas, 
and whose non-atomic initial and cut rules are admissible. We will also assume that whenever contraction is allowed then weakening is also allowed, that is, our systems can be affine, but not relevant. We assume a commutative
calculus because the machinery to check whether a rule permutes over another
given in~\cite{nigam13iclp,nigam14ebl} only deals with such systems. We believe,
however, that the results presented here could be easily extended to
non-commutative proof systems if automated mechanisms to check rule permutation
are given. The assumption that the initial and cut rules are admissible are
standard in any focusing discipline as these have atomic initial rules and no
cuts.

We will avoid the expression ``permute over'' and use either ``permute up'' or
``permute down'' and the notation introduced below for clarity.

\begin{definition}[Permutability]
Let $\alpha$ and $\beta$ be two inference rules in a sequent calculus system
$\mathbb{S}$. We will say that $\alpha$ \emph{permutes up} $\beta$, denoted by
$\alpha \uparrow \beta$, if for every $\mathbb{S}$ proof in which
$\alpha$ occurs immediately below $\beta$ there exists another
$\mathbb{S}$ proof in which $\beta$ occurs immediately below $\alpha$. Consequently,
$\beta$ \emph{permutes down} $\alpha$ ($\beta \downarrow \alpha$). 
\end{definition}

\begin{definition}[Permutation graph]
Let $\mathcal{R}$ be the set of inference rules of a sequent calculus system
$\mathbb{S}$. We construct the \emph{permutation graph} $P_{\mathbb{S}}=(V, E)$
for $\mathbb{S}$ by taking $V = \mathcal{R}$ and $E = \{ (\alpha, \beta) \;|\;
\alpha \uparrow \beta \}$.
\end{definition}

Observe that $P_{\mathbb{S}}$ is a directed graph.

\begin{definition}[Permutation cliques]
Let $\mathbb{S}$ be a sequent calculus system and $P_\mathbb{S}$ its permutation
graph. Consider $P^*_\mathbb{S}=(V^*, E^*)$ the undirected graph obtained from
$P_\mathbb{S}=(V,E)$ by taking $V^* = V$ and $E^* = \{ (\alpha, \beta) \;|\;
(\alpha, \beta) \in E \text{ and } (\beta, \alpha) \in E \}$. Then the
\emph{permutation cliques} of $\mathbb{S}$ are the maximal cliques\footnote{A
clique in a graph $G$ is a set of vertices such that all vertices are pairwise
connected by one edge.} of $P^*_\mathbb{S}$.
\end{definition}

Permutation cliques can be though of as equivalence classes for inference rules
and they are not always disjoint.

\begin{definition}[Permutation partition]
Let $\mathbb{S}$ be a proof system and $P_\mathbb{S}$ its permutation graph.
Then a \emph{permutation partition} $\mathcal{P}$ is a partition of
$P_\mathbb{S}$ such that each component is complete graph. We will call each
component of such partitions a \emph{permutation group}, motivated by the fact
that inferences in the same group permute over each other.
\end{definition}

It is always possible to find such a partition by taking each component to be
one single vertex, but we are mostly interested in bi-partitions.

Given the permutation cliques of a graph (which can be computed in
exponential time and, plus, are normally small graphs), it is possible to obtain
permutation partitions just by assigning at most
one partition to those rules that belong to two or more cliques. Therefore,
there might be many possible ways to partition the rules of a system. In what
follows we will define which are the interesting partitions that will yield a
focused proof system.

\begin{definition}[Permutation partition hierarchy]
Let $\mathbb{S}$ be a proof system, $P_\mathbb{S}$ its permutation graph and
$\mathcal{P} = G_1, ..., G_n$ a permutation partition. We say that $G_i < G_j$
iff for every inference $\alpha_i \in G_i$ and $\alpha_j \in G_j$ we have that
$\alpha_i \downarrow \alpha_j$, \ie,$\alpha_j \uparrow \alpha_i$ or
equivalently $(\alpha_j, \alpha_i) \in P_\mathbb{S}$.
\end{definition}

Observe that the hierarchy  $<$ between permutation groups is \emph{not}
transitive.

\section{Focused Proof Systems Generation}
\label{sec:focusing}

Using the permutation partitions of a given proof system $\mathbb{S}$ it is
possible to derive a focused proof system $\mathbb{S}^f$ if some conditions
are fulfilled. In this section we explain these conditions and prove that the
induced focused system is sound and complete with respect to $\mathbb{S}$.

\begin{definition}[Focusable permutation partition]
\label{def:focusable_partition}
Let $\mathbb{S}$ be a sequent calculus proof system and $G_1, ..., G_n$ a
permutation partition of the rules in $\mathbb{S}$. We say that it is a
\emph{focusable permutation partition} if it fulfills the following criteria:

\begin{itemize}
  \item $n = 2$ and $G_1 < G_2$;\footnote{See Remark~\ref{rem:partition} for more about this requirement.}

  \item Every rule in group $G_2$ has at most one auxiliary formula in each
  premise;

  \item Every non-unary rule in group $G_2$ splits the context among the
  premises (\ie, there is no implicit contraction of context formulas on
  branching rules).

\end{itemize}

We call $G_1$ the negative group and $G_2$ the positive group following usual
terminology from the focusing literature~\cite{andreoli92jlc}. 
\end{definition}

As for now, we will only define permutation partitions of logical inference
rules. The structural inference rules can be treated separately. In particular,
the role of contraction and its relation to the partitions is discussed in
Section \ref{sec:contraction}.

\begin{definition}[Negative/positive formula]
Let $\mathbb{S}$ be a sequent calculus proof system with a focusable permutation
partition. We say that a formula $F$ in an $\mathbb{S}$ proof is negative
(positive) if its main connective is introduced by a negative (positive)
inference rule.
\end{definition}

Observe that, in contrast to the usual approach, we do not assign polarities to
connectives on their own. Therefore the polarity of a formula will change
depending on whether it occurs on the right or on the left side of the sequent.

Based on the focusable permutation partition, we can define a focused proof
system for $\mathbb{S}$. This definition in syntactically different from those
usually present in the literature. It will, in particular, force the store and
subsequent selection of a negative formula. This extra step is only for the sake
of uniformity and clear separation between phases (there will always be a ``no
phase'' state between two phases). It also makes the completeness proof clearer.

\begin{definition}[Focused proof system]
Let $\mathbb{S}$ be a sequent calculus proof system and $G_1 < G_2$
a focusable permutation partition of the rules in $\mathbb{S}$. Then we
can define the \emph{focused} system $\mathbb{S}^f$ in the following way:

\begin{paragraph}{Sequents.}
$\mathbb{S}^f$ sequents are of the shape 
%
$$\Gamma ; \Gamma' \vdash^p \Delta ; \Delta'$$
%
Where $p \in \{ +, -, 0 \}$ indicates a positive, negative and neutral sequents
respectively. We will call $\Gamma'$ and $\Delta'$ the \emph{active} contexts.
\end{paragraph}

\begin{paragraph}{Inference rules.}
For each rule $\alpha$ in $\mathbb{S}$ belonging to the negative (positive)
group, $\mathbb{S}^f$ will have a rule $\alpha$ with conclusion and premises
being negative (positive) sequents and main and auxiliary formulas occurring in
the active contexts.

Additionally, $\mathbb{S}^f$ will have the following structural rules.

\emph{Selection rules} move a formula $F$ to the active context. If $F$ is
negative, than $p = -$. If $F$ is positive, than there is no negative $F' \in
\Gamma \cup \Delta$ and $p = +$.
%
\[
\infer[sel_l]{\Gamma, F ; \cdot \vdash^0 \Delta ; \cdot}{\Gamma ; F \vdash^p \Delta ; \cdot}
\quad
\infer[sel_r]{\Gamma ; \cdot \vdash^0 \Delta, F ; \cdot}{\Gamma ; \cdot \vdash^p \Delta ; F}
\]

% Note: the next rules will guarantee the exhaustion of a phase before
% moving to the next.

\emph{Store rules} remove a formula $F$ from the active context if $F$ is
negative and $p = +$ or if $F$ is positive and $p = -$.
%
\[
\infer[st_l]{\Gamma ; \Lambda, F \vdash^p \Delta ; \Pi}{\Gamma, F; \Lambda \vdash^p \Delta ; \Pi}
\quad
\infer[st_r]{\Gamma ; \Lambda \vdash^p \Delta ; \Pi, F}{\Gamma ; \Lambda \vdash^p \Delta, F ; \Pi}
\]

The \emph{end rule} removes the label $p = \{ +, - \}$ of a sequent by setting it to 0
if the active contexts are empty.

\[
\infer[end]{\Gamma ; \cdot \vdash^p \Delta ; \cdot}{\Gamma ; \cdot \vdash^0 \Delta ; \cdot}
\]
\end{paragraph}


An $\mathbb{S}^f$ proof is characterized by sequences of inferences
labeled with $+$ or $-$ which we will call \emph{phases}. Thus, we
can say that selection rules are responsible for starting a phase and the end
rule finishes a phase. Between any two phases there is always a
``neutral'' state, denoted by a sequent labeled with 0.
\end{definition}

In focused proofs, once a formula is being decomposed, all its
sub-formulas belonging to the same group are also decomposed before the end of
that phase. To prove completeness of such systems, we will show that this is in
fact a natural effect even in unfocused proofs.

Our completeness proof follows the idea of the one in \cite{miller07cslb}, generalizing it to any focusable proof system. We define the following elements.

\begin{definition}[Purely positive/neutral sequent]
Let $G_1, G2$ be a focusable permutation partition of a sequent calculus system
$\mathbb{S}$, $\varphi$ a proof in $\mathbb{S}$ and $\mathcal{S}$ a sequent in
$\varphi$. Then we will say that $\mathcal{S}$ is a \emph{purely positive
sequent} if it only contains positive formulas. Otherwise we will say that it is
a \emph{neutral sequent}.
\end{definition}

\begin{definition}[Negative/positive trunk]
Let $G_1, G_2$ be a focusable permutation partition of a sequent calculus system
$\mathbb{S}$, $\varphi$ a proof in $\mathbb{S}$, $\mathcal{S}^+$ a purely
positive sequent and $\mathcal{S}^0$ a neutral sequent in $\varphi$. Then a
\emph{positive trunk} is a subproof of $\varphi$ with root in $\mathcal{S}^+$
containing only positive inferences, \ie, extending up to the first sequent
which is the conclusion of a negative inference. Analogously, a \emph{negative
trunk} is a subproof of $\varphi$ with root in $\mathcal{S}^0$ containing only
negative inferences, \ie, finishing at the sequents which are the conclusions
of positive rules.
\end{definition}

The reason why positive trunks are defined with a purely positive sequent and
negative trunks allow for an arbitrary root is because negative rules have a
certain ``preference'' and negative formulas can be selected in a focused system
regardless of other positive formulas being present. Whereas in the case of positive
formulas, they can only be selected if there are no other negative formulas in
the sequent.

The next lemma states an important property of positive trunks.

\begin{lemma}
\label{lmm:unique}
Let $T$ be a positive trunk with root $\mathcal{S}$. Then all sequents occurring
in $T$ contain at most one ancestor of each formula in $\mathcal{S}$.
%and each
%formula in $\mathcal{S}$ contain as most one ancestor in each sequent in $T$.
\end{lemma}

\begin{proof}
A positive trunk is only definable for proof systems with a focusable
permutation partition. By Definition \ref{def:focusable_partition}, we know that
every positive rule splits the context (if it is branching) and does not have
more than one auxiliary formula in each premise. As a consequence, the
formulas in the conclusion of a positive rule have exactly one ancestor in each
rule application, which will be in one of the premises: either
the formula itself (if it is not the main formula) or one sub-formula. Therefore,
there is a one to one relation between the formulas in any sequent in $T$ and
the formulas in $\mathcal{S}$.
\end{proof}

\begin{definition}[Trunk border]
Let $T$ be a (positive or negative) trunk of an $\mathbb{S}$ proof. We say that
the set of sequents occurring at the leaves of $T$ is its \emph{border} and we
will denote it by $\mathcal{B}$.
\end{definition}

Note that the sequents in the border of a positive trunk must necessarily have
at least one negative formula.

The following lemma is important for the proof of completeness of focusing.
Intuitively, it states that if the rules of the sequent calculus system fulfills
the focusable properties then there is already some kind of focusing behaviour
even in an unfocused proof. This will be essential for the translation of
unfocused into focused proofs.

\begin{lemma}
\label{lmm:focusing_graph}
Let $\varphi$ be an $\mathbb{S}$ proof and $T$ a positive trunk in $\varphi$ with
a purely positive root sequent $\mathcal{S}^+$. Then there is at least one
positive formula $F$ in $\mathcal{S}^+$ whose layer of positive sub-formulas is
completely decomposed, \ie, all sub-formulas of $F$ in the leaves of $T$ are not
positive (they are negative or an atom).
\end{lemma}

\begin{proof}
Let $F_1, ..., F_n$ be the positive formulas occurring in the sequent
$\mathcal{S}^+$. Given the sequents in the border $\mathcal{B}$ we will build a
graph in the following way: the vertices of the graph are the formulas $F_1,
..., F_n$ and there is an edge $(F_i, F_j)$ if there is a sequent in
$\mathcal{B}$ containing a negative ancestor of $F_i$ and a positive ancestor of
$F_j$. We call this the \emph{focalization graph}\footnote{Observe that this
definition is slightly different than that in \cite{miller07cslb}, in the sense
that we only use the formulas in the root of the trunk for the graph, while
Miller and Saurin use all formulas to which an inference was applied in the
trunk.}.
Therefore, the number of out-edges of a vertex indicates the number of
negative ancestors of that formula, and the number of in-edges indicates the
positive ancestors. To say that the layer of positive connectives of a formula
was completely decomposed is equivalent to say that all its ancestors in the
border are negative (or atomic) which, in turn, is equivalent to say that its
vertex has only out-edges.

It is possible for the focalization graph to have disconnected vertices, without in
or out edges. This will only be the case if the formula corresponding to that
vertex has only atomic ancestors. Trivially, this will already be a
positive formula which was completely decomposed. We will thus focus on the case
where the graph is connected.

To prove that such a vertex exists, we will prove a stronger result, namely,
that the focalization graph is acyclic. The acyclicity of such a graph implies
the existence of a source vertex (only out-edges).

We prove this by contradiction. Assume that the focalization graph of $T$
contains a cycle of minimal length: $F_1 \rightarrow ... \rightarrow F_k \rightarrow F_1$. Let
$\mathcal{S}_1, ..., \mathcal{S}_k$ be the sequents in $\mathcal{B}$ justifying
each edge in the cycle. This means that $\mathcal{S}_i$ has a negative ancestor
of $F_i$ and a positive ancestor of $F_{(i+1 mod k)}$.

Let $\mathcal{S}_0$ be the highest sequent in $T$ such that every
$\mathcal{S}_1, ..., \mathcal{S}_k$ is a leaf of the tree rooted in
$\mathcal{S}_0$. Since the leaves of this tree contain ancestors of the formulas
$F_1, ..., F_k$, so does the root $\mathcal{S}_0$.

Let $\beta$ be the inference applied to $\mathcal{S}_0$. Then $\beta$ must be a
branching inference, otherwise it contradicts the fact that it is the highest 
possible sequent. Without loss of generality, assume that $\beta$ is a binary
inference. Let $\mathcal{S}_L$ and $\mathcal{S}_R$ be the left and right
premises of $\beta$, which is applied to $G$ in $\mathcal{S}_0$. By Lemma
\ref{lmm:unique}, we can partition the formulas $F_1, ..., F_k$ in two groups:
the formulas $\Gamma_L$ with ancestors on the left and the formulas $\Gamma_R$ with ancestors
on the right. Clearly none of these groups are empty, otherwise we could take one of
$\beta$'s premises as the highest sequent with $\mathcal{S}_1, ...,
\mathcal{S}_k$ as leaves.
Let $F$ be the super-formula of $G$ in $\mathcal{S}^+$. Then there are
two cases:

\begin{itemize}
  \item[(1)] $F \notin \{ F_1, ... F_k \}$

  In this case, the sets $\Gamma_L$ and $\Gamma_R$ are disjoint. A cycle between
  these elements would mean that there must be at least two arrows connecting
  one element from $\Gamma_L$ to $\Gamma_R$ and vice versa. W.l.o.g., let $F_l
  \in \Gamma_L$ and $F_r \in \Gamma_R$ such that $F_l \rightarrow F_r$.
  But then this means that $F_l$ and $F_r$ contain ancestors in the same sequent
  in $\mathcal{B}$, contradicting the fact that their ancestors were split
  between the right and left branches upon the application of $\beta$.
  
  \item[(2)] $F \in \{ F_1, ..., F_k \}$

  In this case there is one element in $\Gamma_L \cap \Gamma_R$, namely, $F$.
  W know that two edges are needed to complete a cycle, from an element in
  $\Gamma_L$ to an element in $\Gamma_R$ and vice versa. If $F$ is part of one
  direction of this connection, than we still need an edge between the sides and
  the problem is the same as in the previous case. The other choice is to have
  $F$ as the connection element in both directions, \ie, having the edges: $F_l
  \rightarrow F \rightarrow F_r$ and $F'_l \leftarrow F \leftarrow F'_r$. But
  then there exists a smaller cycle, with only the elements of $\Gamma_L$ or
  only the elements of $\Gamma_R$, which contradicts the minimality of the cycle
  containing $F_1, ..., F_k$.
\end{itemize}

Therefore the focalization graph cannot have a cycle, and it has a
source element which is a formula whose layer of positive connectives is
completely decomposed in $T$.
\end{proof}

Now we can prove that the focused systems obtained from a focusable permutation
partition are sound and complete.

\begin{theorem}[Completeness of focused proof systems]
\label{thm:completeness}
A sequent $\Gamma \vdash \Delta$ is provable in $\mathbb{S}$ iff the sequent
$\Gamma; \cdot \vdash^0 \Delta; \cdot$ is provable in $\mathbb{S}^f$.
\end{theorem}

\begin{proof}
The $\Leftarrow$ direction is trivial. Every $\mathbb{S}^f$ proof can be
transformed into an $\mathbb{S}$ proof by taking the corresponding rules and
skipping select, store and end inferences.

The $\Rightarrow$ direction is more involved. We will show that every
$\mathbb{S}$ proof can be transformed into a focused $\mathbb{S}^f$ proof.

By using the permutability of the rules in each group, we can see that it is
always possible to permute negative rules down in the proof. After permuting
exhaustively those rules, we will end up with a negative trunk whose leaves are
only purely positive sequents. By Lemma \ref{lmm:focusing_graph} we know that
there is at least one positive formula $F$ in each of these sequents whose
positive layer is completely decomposed. Then, the root of each purely positive
sequent can be translated to an end rule followed by a select rule which will
choose this formula $F$ to be in the active context.
\end{proof}

\begin{remark}
\label{rem:partition}
One could imagine to generalize the conditions in
Definition~\ref{def:focusable_partition} by allowing permutation partitions with
more than two groups. However, it is not clear how
the corresponding complete focused proof system would look like and if it can be
generated. For example, consider a permutation graph that can be partitioned in
three groups: $G_1 < G_2 < G_3$ (even totally ordered). It is not possible to guarantee
(looking from bottom up in a proof) that all $G_2$ rules can always be introduced
before $G_3$ rules. Consider for example the following derivation in the
unfocused proof system:
\[
  \infer[G_2^r]{\qquad \Sscr \qquad}
  {\infer[G_3^r]{\qquad \Sscr_1 \qquad}
  {\infer[G_1^r]{\qquad \Sscr_2 \qquad}{\deduce{\qquad \Sscr_4 \qquad}{\Xi}}}}
\]
where $G_i^r$ is some rule of partition $G_i$ for $1 \leq i \leq 3$. The sequent
$\Sscr_1$ might still have some formulas that can be introduced by $G_2$ rules
and since $G_2 < G_3$, we would like to decompose them before applying
$G_3^r$. However, $G_3^r$ might have decomposed a formula whose subformula is
introduced by the rule $G_1^r$. Thus it is not necessarily possible to permute
$G_2$ rules appearing in $\Xi$ downwards.
\end{remark}


\section{Admissibility of contraction}
\label{sec:contraction}

During proof search, it is desirable to avoid unnecessary copying of formulas
at each rule application. Either by not copying the same context in all premises
or by not auto-contracting the main formula of a rule application. The analysis
of where the contraction rule lies in the permutation cliques can give us
insights on when it can be avoided. 

\begin{definition}[Admissibility of contraction]
Let $\mathbb{S}$ be a sequent calculus system with a set of rules $\mathcal{R}$.
We say that contraction is \emph{admissible} for $\mathcal{R}' \subseteq
\mathcal{R}$ if for every $\mathbb{S}$ proof $\varphi$ there exists an
$\mathbb{S}$ proof $\varphi'$ such that contraction is never applied to main
formulas of inferences in $\mathcal{R}'$.
\end{definition}

The intuitionistic system LJ is an interesting example of a calculus in which
contraction is not admissible for all formulas. It is only complete if the main
formula of the implication left rule is contracted \cite{dyckhoff92jsl}.

% This is wrong. See counter example below.
% To show that contraction is admissible for a rule $\alpha$, we must show that a
% contraction in the main formula of $\alpha$ can be reduced to a contraction of
% the auxiliary formulas of $\alpha$. 
The admissibility of contraction involves transformations which are similar to the
rank reduction rewriting rules of reductive cut-elimination. This is a special
case of permutation checking, since the uppermost inference is supposed to be
applied to auxiliary formulas of the lowermost inference.

\begin{definition}[Contraction permutation]
Let $\mathbb{S}$ be a sequent calculus proof system, $c$ one of its contraction
rules and $\alpha$ a logical rule applied to a formula $F_\alpha$. We say that
$c \uparrow_c \alpha$ if a derivation composed by contraction of $F_\alpha$
followed by applications of $\alpha$ to the contracted formulas can be
transformed into a derivation where $\alpha$ is applied to $F_\alpha$ and
contraction is applied to the auxiliary formulas of $\alpha$.
\end{definition}

Given these definitions, it might be natural to think that if $c \uparrow_c
\alpha$ for some inference $\alpha$, then it is admissible for this inference.
But this is not the case. Observe that $c \uparrow_c \rightarrow_l$ in LJ:

{\small
\[
\infer[c_l]{A\rightarrow B, \Gamma \vdash C}{
  \infer[\rightarrow_l]{A \rightarrow B, A \rightarrow B, \Gamma \vdash C}{
    \infer[\rightarrow_l]{A\rightarrow B, \Gamma \vdash A}{
      \deduce{\Gamma \vdash A}{\varphi_1}
      &
      \deduce{B, \Gamma \vdash A}{\varphi_2}
    }
    &
    \infer[\rightarrow_l]{B, A \rightarrow B, \Gamma \vdash C}{
      \deduce{B, \Gamma \vdash A}{\varphi_3}
      &
      \deduce{B, B, \Gamma \vdash C}{\varphi_4}
    }
  }
}
\quad
\rightsquigarrow
\quad
\infer[\rightarrow_l]{A \rightarrow B, \Gamma \vdash C}{
  \deduce{\Gamma \vdash A}{\varphi_1}
  &
  \infer[c_l]{B, \Gamma \vdash C}{
    \deduce{B, B, \Gamma \vdash C}{\varphi_4}
  }
}
\]
}

Nevertheless, contraction is not admissible for $\rightarrow_l$, as it was
already mentioned. The problem is clear when we try to prove the sequent $\neg
(A \vee \neg A) \vdash$ for instance (considering $\neg A \equiv A \rightarrow
false$). In order to be able to apply the transformation above, it is necessary
that both implication formulas are introduced one after the other. Since the
$\rightarrow_l$ rule is not invertible in LJ, sometimes it is not possible to
achieve such configuration. Reasoning about admissibility of contraction
requires, thus, the analysis of permutation of rules in the whole calculus. 

\begin{definition}[Admissibility of contraction in a phase]
Let $\mathbb{S}$ be a sequent calculus proof system, $G_1, G_2$ a focusable
permutation partition and $c$ its contraction rules (left and right). We say
that contraction is admissible in phase $i$ if every $\mathbb{S}$ proof can be
transformed into a proof where contraction is applied only to main formulas of
rules $\alpha \in G_i$.
\end{definition}

\begin{theorem}
Let $\mathbb{S}$ be a sequent calculus proof system, $G_1, G_2$ a focusable
permutation partition and $c$ its contraction rules (left and right). If $c
\uparrow \alpha$ and $c \uparrow_c \alpha$ for every rule $\alpha \in G_i$, then
contraction is admissible in phase $i$.
\end{theorem}

\begin{proof}
Let $\varphi$ be an $\mathbb{S}$ proof. Since $\mathbb{S}$ has a focusable
permutation partition, we can define a focused calculus $\mathbb{S}^f$. By the
completeness result in Theorem \ref{thm:completeness}, it is possible to
translate $\varphi$ into a focused proof $\varphi^f$ divided in phases. Since
there is no special treatment for structural rules, every contraction in
$\varphi$ will appear in the same corresponding formulas of $\varphi^f$. 

Assume that $c \uparrow_c \alpha$ and $c \uparrow \alpha$ for every $\alpha$ in
$G_i$. This means that it is possible to permute the contraction up until the
leaves of this phase, which are sequents whose active formulas are necessarily
of the other phase. These formulas are then stored, and selected later on. This
contraction can than be replaced by only the storing of the formula and applied
once the formula is selected again. This moves the contractions from one phase
to another.

If we translate this focused proof back to an unfocused calculus, we
obtain an $\mathbb{S}$ proof with no contractions applied to $G_i$ formulas.
Therefore, we can say that contraction is admissible in the phase $G_i$.
\end{proof}

It is clear that if contraction permutes up all the rules, \ie, it is
admissible for both phases, then it is admissible in the calculus.

\subsection{Automated analysis}
\label{sec:automation}

Given a proof system and a permutation partition, it is computationally feasible
to check whether this will induce a focused proof system.

In previous work \cite{nigam13iclp,nigam14ijcar}, we have shown how to automate
the checking for permutability of rules. Using the method developed, we can also
build the permutation graph of a system and compute the permutation cliques (by
using an algorithm to find all maximal cliques of graph, e.g., Bron-Kerbosch).
Our tool Quati \cite{nigam14ijcar} has recently been incremented with this
functionality. Given a sequent calculus system specification, Quati is able to
compute its (partial\footnote{On the current implementation, permutations that
rely on the invertibility of rules are not yet identified. We have plans to
integrate such checks soon by using techniques described in our previous work~\cite{nigam14jlc}.}) permutation graph and the permutation cliques.
Using these results, we can find focused versions of the proof systems and
reason about the admissibility of contraction.

%\subsection{Invertible rules}
%
% Dale mentioned that this might be one interesting thing, so I am adding a
% section on it.
%An inference rule is said to be invertible if all its premises can be derived
%from its conclusion. 

% Giselle: there is a circular dependency on the automated deduction of
% invertible rules only via permutation arguments. We know so far that if a rule
% permutes down all other rules in a calculus, than it is invertible. But
% sometimes to deduce these permutation relations it is necessary to use the
% fact that a rule is invertible. In this case, invertibility is shown using the
% cut rule, which we can also do, but we have not argued on that so far.

\section{Case studies}
\label{sec:cases}

As case studies we will show how the focused proof systems LKF, LJF and MALLF
can be obtained from LK, LJ and MALL respectively using the permutation cliques.

\subsection{MALL}

MALL stands for multiplicative additive linear logic and its rules are depicted
in Figure \ref{fig:mall}. It is basically linear logic without exponentials. A
focused system for this calculus was proposed by \cite{andreoli92jlc}.

\begin{figure}[h]
{\footnotesize
\begin{align*}
\infer[\binampersand_l]{\Gamma, A_1 \binampersand A_2 \vdash \Delta}{\Gamma, A_i \vdash \Delta}
&\quad&
\infer[\binampersand_r]{\Gamma \vdash \Delta, A \binampersand B}{\Gamma \vdash \Delta, A & \Gamma \vdash \Delta, B}\\
\infer[\otimes_l]{\Gamma, A \otimes B \vdash \Delta}{\Gamma, A, B \vdash \Delta}
&\quad&
\infer[\otimes_r]{\Gamma, \Gamma' \vdash \Delta, \Delta', A \otimes B}{\Gamma \vdash \Delta, A & \Gamma' \vdash \Delta', B}\\
\infer[\oplus_l]{\Gamma, A \oplus B \vdash \Delta}{\Gamma, A \vdash \Delta & \Gamma, B \vdash \Delta}
&\quad&
\infer[\oplus_r]{\Gamma \vdash \Delta, A_1 \oplus A_2}{\Gamma \vdash \Delta, A_i}\\
\infer[\bindnasrepma_l]{\Gamma, \Gamma', A \bindnasrepma B \vdash \Delta, \Delta'}{\Gamma, A \vdash \Delta & \Gamma', B \vdash \Delta'}
&\quad&
\infer[\bindnasrepma_r]{\Gamma \vdash \Delta, A \bindnasrepma B}{\Gamma \vdash \Delta, A, B}
\end{align*}
}
\caption{MALL inference rules}
\label{fig:mall}
\end{figure}

Given the logical inferences of MALL, the permutation cliques found were the
following:
%
\begin{align*}
C_1 &: \{ \otimes_l, \oplus_l, \bindnasrepma_r, \binampersand_r, \binampersand_l, \oplus_r \}\\
C_2 &: \{ \otimes_r, \oplus_r, \bindnasrepma_l, \binampersand_l \}
\end{align*}
%
With the relation $C_1 < C_2$. A focusable permutation partition can be
obtained by choosing:
%
\begin{align*}
G_1 &: \{ \otimes_l, \oplus_l, \bindnasrepma_r, \binampersand_r \}\\
G_2 &: \{ \otimes_r, \oplus_r, \bindnasrepma_l, \binampersand_l \}
\end{align*}
%
The focused proof systems obtained with these partitions is precisely MALLF.

\subsection{LK}

% Additive and multiplicative conjunctions and disjunctions
In order to derive the focused system LKF for classical logic from LK, all
variations of inferences must be considered. We need to take into account the
additive and multiplicative versions of each conjunction and disjunction, as
depicted in Figure \ref{fig:lk}.

\begin{figure}[h]
{\footnotesize
\begin{align*}
\infer[\wedge^a_l]{\Gamma, A_1 \wedge A_2 \vdash \Delta}{\Gamma, A_i \vdash \Delta}
&\quad&
\infer[\wedge^a_r]{\Gamma \vdash \Delta, A \wedge B}{\Gamma \vdash \Delta, A & \Gamma \vdash \Delta, B}\\
\infer[\wedge^m_l]{\Gamma, A \wedge B \vdash \Delta}{\Gamma, A, B \vdash \Delta}
&\quad&
\infer[\wedge^m_r]{\Gamma, \Gamma' \vdash \Delta, \Delta', A \wedge B}{\Gamma \vdash \Delta, A & \Gamma' \vdash \Delta', B}\\
\infer[\vee^a_l]{\Gamma, A \vee B \vdash \Delta}{\Gamma, A \vdash \Delta & \Gamma, B \vdash \Delta}
&\quad&
\infer[\vee^a_r]{\Gamma \vdash \Delta, A_1 \vee A_2}{\Gamma \vdash \Delta, A_i}\\
\infer[\vee^m_l]{\Gamma, \Gamma', A \vee B \vdash \Delta, \Delta'}{\Gamma, A \vdash \Delta & \Gamma', B \vdash \Delta'}
&\quad&
\infer[\vee^m_r]{\Gamma \vdash \Delta, A \vee B}{\Gamma \vdash \Delta, A, B}
\end{align*}
}
\caption{The complete LK system, with additive and multiplicative inferences.}
\label{fig:lk}
\end{figure}

The permutation cliques of the complete LK system are:
%
\begin{align*}
C_1 &: \{ \wedge^a_r, \wedge^m_l, \vee^m_r, \vee^a_l, \wedge^a_l, \vee^a_r \}\\
C_2 &: \{ \wedge^m_r, \wedge^a_l, \vee^a_r, \vee^m_l \}
\end{align*}
%
And the relation between then is $C_1 < C2$. Analogous to the MALL situation, we
can drop the two last rules from $C_1$ and obtain a focusable permutation
partition which corresponds to the propositional fragment of LKF.

By analysing the permutation relation of contraction to the rules in the
partitions, we observe that it permutes up ($\uparrow$ and $\uparrow_c$) all the
inferences in $C_1 \ \{\wedge^a_l, \vee^a_r \}$, therefore it is admissible in
the negative phase. For the positive phase, on the other hand, contraction will
not permute up, for example, $\wedge^a_l$. We can thus conclude that such a
system must have contraction for positive formulas\footnote{This contraction is
implicit on the \emph{decide} rule and the positive rules for the usual presentation of LKF}.
% I checked the presentation of LKF in the paper "Focusing and polarization for
% intuitionistic logic" and in a journal paper currently being written by Dale and
% his students. In both versions there is no contraction of the main formula on
% introduction rules, but an auto contraction when deciding on positive
% formulas.
% VN: There are implicit contractions of side-formulas. 

\subsection{LJ}

The case of the intuitionistic calculus LJ is similar to LK. We will need to
distinguish the additive and multiplicative rules for the conjunction, but as we
are dealing with intuitionistic logic, we use the additive inference for
disjunction and explicit inferences for implication.

% Additive and multiplicative conjunctions
% Disjunction
% Implication
\begin{figure}[h]
{\footnotesize
\begin{align*}
\infer[\wedge^a_l]{\Gamma, A_1 \wedge A_2 \vdash C}{\Gamma, A_i \vdash C}
&\quad&
\infer[\wedge^a_r]{\Gamma \vdash A \wedge B}{\Gamma \vdash A & \Gamma \vdash B}\\
\infer[\wedge^m_l]{\Gamma, A \wedge B \vdash C}{\Gamma, A, B \vdash C}
&\quad&
\infer[\wedge^m_r]{\Gamma, \Gamma' \vdash A \wedge B}{\Gamma \vdash A & \Gamma' \vdash B}\\
\infer[\vee_l]{\Gamma, A \vee B \vdash C}{\Gamma, A \vdash C & \Gamma, B \vdash C}
&\quad&
\infer[\vee_r]{\Gamma \vdash A_1 \vee A_2}{\Gamma \vdash A_i}\\
\infer[\rightarrow_l]{\Gamma, \Gamma', A \rightarrow B \vdash C}{\Gamma \vdash A & \Gamma', B \vdash C}
&\quad&
\infer[\rightarrow_r]{\Gamma \vdash A \rightarrow B}{\Gamma, A \vdash B}
\end{align*}
}
\caption{The complete LJ system, with additive and multiplicative inferences.}
\label{fig:lj}
\end{figure}

The permutation cliques of the complete LJ system are:
%
\begin{align*}
C_1 &: \{ \wedge^m_l, \wedge^a_r, \vee_l, \rightarrow_r, \wedge^a_l, \vee_r \}\\
C_2 &: \{ \wedge^a_l, \wedge^m_r, \vee_r, \rightarrow_l \}
\end{align*}
%
And relation $C_1 < C_2$. The focusable permutation partition corresponding
to LJF can be obtained by taking $C_1$ minus the last two elements and $C_2$ as
is.

The relation of contraction on the permutation graph of LJ is analogous to that
of LK: it is admissible for the negative phase but not for the positive phase.

\section{Conclusion}
\label{sec:conc}

We tackled the problem of automatically devising focused proof systems for
sequent calculi. Our aim was to provide a uniform and automated way to obtain
the sound and complete systems without using an encoding in linear logic, as it
is usually done. Using the proof of completeness of focused MALL in
\cite{miller07cslb} as an inspiration, we defined decidable properties a proof
system must have so that it is possible to construct a focused version of it.

The main element in our solution is the permutation graph of a sequent calculus
system. By using this graph we can separate the inferences into positives and
negatives and also reason on the admissibility of contraction. The permutation
graph represents the permutation lemmas used in the proof in
\cite{miller07cslb}. It is a known fact that proving such lemmas is a tedious
and error-prone task, therefore we propose the use of the machinery in
\cite{nigam14ijcar} to help on the construction of such graph. Given
this data structure, the conditions the permutation graph and the inference
rules of a proof system must have for that proof system to admit a focused
version can be easily checked.
An implementation of the full method is an ongoing work.

Although we can deduce in which phase the contraction of formulas is admissible,
it is still unclear if the position of this rule in the permutation graph can
indicate exactly which rules do not admit contraction. We expect to further
investigate the permutation graphs of other systems to find out if this and
other properties can be discovered.

% For posterity, please keep this commented block here. It has an explanation of
% the difficulties in defining a focused system with more than 2 phases.
\begin{comment}

{\color{red}Giselle: at this moment, this section is a discussion on how Alexis'
proof can be adapted for our setting.}

\begin{definition}[$G_i$ sequent]
Let $G_1, ..., G_n$ be a stratifiable permutation partition of a sequent
calculus system $\mathbb{S}$, $\varphi$ a proof in $\mathbb{S}$ and
$\mathcal{S}$ a sequent in $\varphi$. Then we will say that $\mathcal{S}$ is a
\emph{$G_i$ sequent} if it only contains at least one formula in group $G_i$
and all other formulas in groups $G_j$ with $G_j \geq G_i$. Otherwise we say
that $\mathcal{S}$ is a \emph{no group sequent}.
\end{definition}

\begin{definition}[$G_i$ trunk]
Let $G_1, ..., G_n$ be a stratifiable permutation partition of a sequent
calculus system $\mathbb{S}$, $\varphi$ a proof in $\mathbb{S}$ and
$\mathcal{S}$ a $G_i$ sequent in $\varphi$. Then a \emph{$G_i$ trunk} is
a subproof of $\varphi$ with root in $\mathcal{S}$ containing only $G_i$
inferences.
\end{definition}

Using this definition we cannot guarantee what Alexis' lemma states. Take for
example the following derivation:

{\small
\[
\infer[\otimes]{\vdash (A \oplus B) \otimes (C \oplus D), E \bindnasrepma F, G \bindnasrepma H}{
  \infer[\bindnasrepma]{\vdash A \oplus B, E \bindnasrepma F}{
    \vdash A \oplus B, E, F
  }
  &
  \infer[\bindnasrepma]{\vdash C \oplus D, G \bindnasrepma H}{
    \vdash C \oplus D, G, H
  }
}
\]
}

Now imagine a parallel world where $\bindnasrepma \in G_2$, $\otimes \in G_1$
and $G_1 < G_2$ . Then we have a $G_1$ trunk where the $G_1$ formula is not
completely decomposed. Given this, we relax the definition of trunk:

\begin{definition}[$G_i$ trunk]
Let $G_1, ..., G_n$ be a stratifiable permutation partition of a sequent
calculus system $\mathbb{S}$, $\varphi$ a proof in $\mathbb{S}$ and
$\mathcal{S}$ a $G_i$ sequent in $\varphi$. Then a \emph{$G_i$ trunk} is
a subproof of $\varphi$ with root in $\mathcal{S}$ containing only $G_j$
inferences such that $G_j \geq G_i$.
\end{definition}

Note that this definition allows a $G_i$ trunk with no application of $G_i$
inferences at all. Although $\mathcal{S}$ (the root of the trunk) might contain
$G_i$ formulas, it might be that only $G_j$ inferences were applied to other
formulas in the trunk. At the leaves of the trunk we have applications of $G_h <
G_i$ inferences, which means we cannot argue to permute the $G_i$ inferences
down (the $G_h$ formulas for these rules are, for instance, subformulas of $G_j$
rules).

Given this characteristic of the trunks, we need a more relaxed version of
Alexis' lemma

\begin{lemma}
\label{lmm:focusing_graph}
Let $\varphi$ be an $\mathbb{S}$ proof and $T$ a $G_i$ trunk in $\varphi$ with
root sequent $\mathcal{S}_i$, $i \geq 2$. Then there is at least one $G_j > G_i$
formula $F$ in $\mathcal{S}_i$ whose layer of $G_i$ subformulas is completely
decomposed, \ie, all subformulas of $F$ in the leaves of $T$ are not $G_i$
formulas.
\end{lemma}

By using this more relaxed version of the lemma, a problem surfaces: we show
that there is a higher formula in the hierarchy that is decomposed, but not the
least possible one. We can't guarantee that the lowest
most group will be chosen in each selection step because the formula that is
decomposed in a $G_i$ trunk might be a $G_j$ formula with $G_j > G_i$. The
problem does not occur in Alexis' proof because he has only two groups, whereas
we are allowing many of them.

Possible fixes for the problem:

\begin{itemize}
  \item We allow only two groups and collapse all groups bigger than 1 into one.
  (I am afraid that this will look like a rephrased version of Alexis and Dale's
  paper.)
  \item We find another use for the graphs, such as during proof search and the
  proof of permutation lemmas, but do not try to prove completeness of focused
  proof systems.
  \item More ideas?
\end{itemize}

\end{comment}

% At this point we need focusing graphs. In Alexis' approach the
% acyclicity of focalization graphs, in the end, guarantees that, even in an
% unfocused MALL proof, there is at least one formula in the positive trunk
% ``whose positive layer of connectives is completely decomposed''. To prove
% this, characteristics particular to linear logic are used, such as: (1) positive
% rules have premises with at most one auxiliary formula; (2) there is no
% contraction on positive formulas and (3) $\otimes$ splits the context. He notes
% also that ``this can be regarded as a kind of implicit focusing result''.
% In our setting, this implicit focalization will be guaranteed by the
% conditions imposed on the stratifiable permutation partition.

\bibliographystyle{llncs/splncs03}
\bibliography{../master}

\end{document}
